\begin{tabbing}
$\forall$\=$k$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it mTyp}$, ${\it vTyp}$:Type, $l$:IdLnk, ${\it tg}$:Id,\+
\\[0ex]$f$:((:State(${\it ds}$) $\times$ ${\it vTyp}$)$\rightarrow$(${\it mTyp}$ + Top)).
\-\\[0ex]($\neg$($k$ = rcv($l$,${\it tg}$)))
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ (destination(lnk($k$)) = source($l$) $\in$ Id))
\\[0ex]$\Rightarrow$ Normal(${\it vTyp}$)
\\[0ex]$\Rightarrow$ Normal(${\it mTyp}$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.$k$(v:${\it vTyp}$) sends on $l$ [${\it tg}$:${\it mTyp}$, $f$ $<$state, v$>$]?[]
\end{tabbing}